﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework.Goals;
using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace MicroBenchmarks.UseDef
{
    [PexClass]    
    [TestClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class InternalFieldsTest
    {
        /// <summary>
        /// An example state that can be achived by calling IncrM1 5 times. However, for calling IncrM1,
        /// there is a pre-condition that some other method has to be called. In this scenario, it
        /// is SetMember2
        /// </summary>
        /// <param name="ifd"></param>
        [PexAssertReachEventually]
        [PexMethod]
        public void UseDefPUT1([PexAssumeUnderTest]InternalFields1 ifd)
        {
            if (ifd.InternalState)
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// An example state that can be achived by calling IncrM1 5 times. However, for calling IncrM1,
        /// there is a pre-condition that some other method has to be called. In this scenario, it
        /// is SetMember2, but here SetMember2 further requires SetMember3
        /// </summary>
        /// <param name="ifd"></param>
        [PexAssertReachEventually]
        [PexMethod]
        public void UseDefPUT2([PexAssumeUnderTest]InternalFields2 ifd)
        {
            if (ifd.InternalState)
                PexAssert.ReachEventually();
        }
    }
}
